Nuprl Lemma : subtype-inherence
0,22
postcript
pdf
A
,
B
:Type.
AtomFree(Type;
B
)
AtomFree(Type;
A
)
A
B
(
x
:
A
,
a
:Atom1.
x
:
B
>>
a
x
:
A
>>
a
)
latex
Definitions
Atom$n
,
AtomFree(
T
;
x
)
,
x
:
T
>>
a
,
x
:
A
B
(
x
)
,
x
:
A
.
B
(
x
)
,
S
T
,
Type
,
,
b
,
M(
a
;
g
;
x
)
,
P
Q
,
S
T
,
x
:
A
.
B
(
x
)
,
x
:
A
B
(
x
)
,
t
T
Lemmas
matters
wf
,
assert
wf
,
bool
wf
,
atom-free
wf
,
inheres
wf
origin
A, B:Type.
AtomFree(Type;A) A 
B (x:A, a:Atom1. x:B>>a x:A>>a) A, B:Type.
AtomFree(Type;A) A B (x:A, a:Atom1. x:B>>a x:A>>a) 
B(x)
x:A. B(x)
T
b Q Tx:A. B(x)
B(x)
T